\section{Implementation}\label{sec:implementation}

The scope of this paper is the \dbsp theory of IVM, so we only briefly touch upon
the implementation aspects.  We defer a full description and evaluation of the
system to a future paper.

\paragraph{\dbsp Rust library}

We have built an implementation of \dbsp as part of an
open-source project with an MIT license:
\anonymize{\url{https://github.com/vmware/database-stream-processor}}.
The implementation consists of a Rust library and a runtime.
The library provides APIs for basic algebraic data types:
such as groups, finite maps, \zr, indexed \zr.
A separate circuit construction API allows users to
create \dbsp circuits by placing operator nodes (corresponding to boxes in our diagrams)
and connecting them with streams, which correspond to the
arrows in our diagrams.  The library provides pre-built generic operators
for integration, differentiation, delay, nested integration and differentiation,
and a rich library of \zr basic incremental operators:
corresponding to plus, negation, grouping, joining, aggregation, $\distinct$,
flatmap, window aggregates, etc.

For iterative computations the library provides the $\delta_0$ operator and
an operator that approximates $\int$ by terminating iteration of
a loop at a user-specified condition (usually the condition is the
requirement for a zero to appear in a specified stream).
The low level library allows users to construct incremental
circuits manually by stitching together incremental versions of primitive operators.

The library supports data-parallel multicore evaluation of circuits
using a natural sharding strategy, and a variety of adapters for
external data sources (e.g., Kafka, CSV files, etc).  The library can
also spill internal operator state to persistent storage.  Benchmark
results (which are very promising) are available in the code
repository and will be discussed in future work.

\paragraph{SQL compiler}

We have also built a SQL to \dbsp compiler, which translates standard
SQL queries into \dbsp circuits.  The compiler implements
Algorithm~\ref{algorithm-inc}, to generate a streaming version of any
SQL query.  The compiler is open-source
\anonymize{\url{https://github.com/vmware/sql-to-dbsp-compiler}} with
an MIT license.  The compiler front-end parser and optimizer are based
on the Apache Calcite~\cite{begoli-icmd18} infrastructure.  The
project is mature enough to pass all 7 million SQL Logic
Tests~\cite{sqllogictest}.  The compiler handles all aspects of SQL,
including NULLs, ternary logic, grouping, aggregation, multiset
queries, etc.  Currently correlated sub-queries and outer joins are
essentially converted to equivalent relational plans using multiple
joins.

\paragraph{Formal verification}

We have formalized and verified all the definitions, lemmas,
propositions, theorems, and examples in this paper using the Lean theorem prover; we make
these proofs available at~\anonymize{\cite{dbsp-theory}}.
% This amounted to roughly 5K lines of Lean code.
The formalization builds on mathlib~\cite{mathlib2020}, which provides
support for groups and functions with finite support (modeling
\zrs). We believe the simplicity of \dbsp enabled completing these
proofs in relatively few lines of Lean code (5K) and keeping a close
correspondence between the paper proofs in~\cite{tr} and Lean.
